Termination w.r.t. Q proof of /tmp/tmpS0gvbF/JFP

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

minus_active(0, y) → 0
mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
mark(s(x)) → s(mark(x))
ge_active(x, 0) → true
mark(minus(x, y)) → minus_active(x, y)
ge_active(0, s(y)) → false
mark(ge(x, y)) → ge_active(x, y)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(0, s(y)) → 0
mark(if(x, y, z)) → if_active(mark(x), y, z)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
if_active(true, x, y) → mark(x)
minus_active(x, y) → minus(x, y)
if_active(false, x, y) → mark(y)
ge_active(x, y) → ge(x, y)
if_active(x, y, z) → if(x, y, z)
div_active(x, y) → div(x, y)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

minus_active(0, y) → 0
mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
mark(s(x)) → s(mark(x))
ge_active(x, 0) → true
mark(minus(x, y)) → minus_active(x, y)
ge_active(0, s(y)) → false
mark(ge(x, y)) → ge_active(x, y)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(0, s(y)) → 0
mark(if(x, y, z)) → if_active(mark(x), y, z)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
if_active(true, x, y) → mark(x)
minus_active(x, y) → minus(x, y)
if_active(false, x, y) → mark(y)
ge_active(x, y) → ge(x, y)
if_active(x, y, z) → if(x, y, z)
div_active(x, y) → div(x, y)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

GE_ACTIVE(s(x), s(y)) → GE_ACTIVE(x, y)
MINUS_ACTIVE(s(x), s(y)) → MINUS_ACTIVE(x, y)
MARK(ge(x, y)) → GE_ACTIVE(x, y)
MARK(s(x)) → MARK(x)
IF_ACTIVE(true, x, y) → MARK(x)
MARK(minus(x, y)) → MINUS_ACTIVE(x, y)
DIV_ACTIVE(s(x), s(y)) → IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
MARK(if(x, y, z)) → IF_ACTIVE(mark(x), y, z)
DIV_ACTIVE(s(x), s(y)) → GE_ACTIVE(x, y)
MARK(div(x, y)) → DIV_ACTIVE(mark(x), y)
MARK(div(x, y)) → MARK(x)
MARK(if(x, y, z)) → MARK(x)
IF_ACTIVE(false, x, y) → MARK(y)

The TRS R consists of the following rules:

minus_active(0, y) → 0
mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
mark(s(x)) → s(mark(x))
ge_active(x, 0) → true
mark(minus(x, y)) → minus_active(x, y)
ge_active(0, s(y)) → false
mark(ge(x, y)) → ge_active(x, y)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(0, s(y)) → 0
mark(if(x, y, z)) → if_active(mark(x), y, z)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
if_active(true, x, y) → mark(x)
minus_active(x, y) → minus(x, y)
if_active(false, x, y) → mark(y)
ge_active(x, y) → ge(x, y)
if_active(x, y, z) → if(x, y, z)
div_active(x, y) → div(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

GE_ACTIVE(s(x), s(y)) → GE_ACTIVE(x, y)
MINUS_ACTIVE(s(x), s(y)) → MINUS_ACTIVE(x, y)
MARK(ge(x, y)) → GE_ACTIVE(x, y)
MARK(s(x)) → MARK(x)
IF_ACTIVE(true, x, y) → MARK(x)
MARK(minus(x, y)) → MINUS_ACTIVE(x, y)
DIV_ACTIVE(s(x), s(y)) → IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
MARK(if(x, y, z)) → IF_ACTIVE(mark(x), y, z)
DIV_ACTIVE(s(x), s(y)) → GE_ACTIVE(x, y)
MARK(div(x, y)) → DIV_ACTIVE(mark(x), y)
MARK(div(x, y)) → MARK(x)
MARK(if(x, y, z)) → MARK(x)
IF_ACTIVE(false, x, y) → MARK(y)

The TRS R consists of the following rules:

minus_active(0, y) → 0
mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
mark(s(x)) → s(mark(x))
ge_active(x, 0) → true
mark(minus(x, y)) → minus_active(x, y)
ge_active(0, s(y)) → false
mark(ge(x, y)) → ge_active(x, y)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(0, s(y)) → 0
mark(if(x, y, z)) → if_active(mark(x), y, z)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
if_active(true, x, y) → mark(x)
minus_active(x, y) → minus(x, y)
if_active(false, x, y) → mark(y)
ge_active(x, y) → ge(x, y)
if_active(x, y, z) → if(x, y, z)
div_active(x, y) → div(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 3 SCCs with 3 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE_ACTIVE(s(x), s(y)) → GE_ACTIVE(x, y)

The TRS R consists of the following rules:

minus_active(0, y) → 0
mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
mark(s(x)) → s(mark(x))
ge_active(x, 0) → true
mark(minus(x, y)) → minus_active(x, y)
ge_active(0, s(y)) → false
mark(ge(x, y)) → ge_active(x, y)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(0, s(y)) → 0
mark(if(x, y, z)) → if_active(mark(x), y, z)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
if_active(true, x, y) → mark(x)
minus_active(x, y) → minus(x, y)
if_active(false, x, y) → mark(y)
ge_active(x, y) → ge(x, y)
if_active(x, y, z) → if(x, y, z)
div_active(x, y) → div(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE_ACTIVE(s(x), s(y)) → GE_ACTIVE(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

GE_ACTIVE(s(x), s(y)) → GE_ACTIVE(x, y)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MINUS_ACTIVE(s(x), s(y)) → MINUS_ACTIVE(x, y)

The TRS R consists of the following rules:

minus_active(0, y) → 0
mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
mark(s(x)) → s(mark(x))
ge_active(x, 0) → true
mark(minus(x, y)) → minus_active(x, y)
ge_active(0, s(y)) → false
mark(ge(x, y)) → ge_active(x, y)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(0, s(y)) → 0
mark(if(x, y, z)) → if_active(mark(x), y, z)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
if_active(true, x, y) → mark(x)
minus_active(x, y) → minus(x, y)
if_active(false, x, y) → mark(y)
ge_active(x, y) → ge(x, y)
if_active(x, y, z) → if(x, y, z)
div_active(x, y) → div(x, y)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MINUS_ACTIVE(s(x), s(y)) → MINUS_ACTIVE(x, y)

From the DPs we obtained the following set of size-change graphs:

MINUS_ACTIVE(s(x), s(y)) → MINUS_ACTIVE(x, y)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MARK(div(x, y)) → DIV_ACTIVE(mark(x), y)
MARK(div(x, y)) → MARK(x)
MARK(if(x, y, z)) → MARK(x)
MARK(s(x)) → MARK(x)
IF_ACTIVE(true, x, y) → MARK(x)
DIV_ACTIVE(s(x), s(y)) → IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
MARK(if(x, y, z)) → IF_ACTIVE(mark(x), y, z)
IF_ACTIVE(false, x, y) → MARK(y)

The TRS R consists of the following rules:

minus_active(0, y) → 0
mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
mark(s(x)) → s(mark(x))
ge_active(x, 0) → true
mark(minus(x, y)) → minus_active(x, y)
ge_active(0, s(y)) → false
mark(ge(x, y)) → ge_active(x, y)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(0, s(y)) → 0
mark(if(x, y, z)) → if_active(mark(x), y, z)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
if_active(true, x, y) → mark(x)
minus_active(x, y) → minus(x, y)
if_active(false, x, y) → mark(y)
ge_active(x, y) → ge(x, y)
if_active(x, y, z) → if(x, y, z)
div_active(x, y) → div(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(if(x, y, z)) → MARK(x)
MARK(if(x, y, z)) → IF_ACTIVE(mark(x), y, z)

The remaining pairs can at least be oriented weakly.

MARK(div(x, y)) → DIV_ACTIVE(mark(x), y)
MARK(div(x, y)) → MARK(x)
MARK(s(x)) → MARK(x)
IF_ACTIVE(true, x, y) → MARK(x)
DIV_ACTIVE(s(x), s(y)) → IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
IF_ACTIVE(false, x, y) → MARK(y)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(DIV_ACTIVE(x₁, x₂)) = 0
POL(IF_ACTIVE(x₁, x₂, x₃)) = x₂ + x₃
POL(MARK(x₁)) = x₁
POL(div(x₁, x₂)) = x₁
POL(div_active(x₁, x₂)) = 0
POL(false) = 0
POL(ge(x₁, x₂)) = 0
POL(ge_active(x₁, x₂)) = 0
POL(if(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(if_active(x₁, x₂, x₃)) = 0
POL(mark(x₁)) = 0
POL(minus(x₁, x₂)) = 0
POL(minus_active(x₁, x₂)) = 0
POL(s(x₁)) = x₁
POL(true) = 0

The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

MARK(div(x, y)) → DIV_ACTIVE(mark(x), y)
MARK(div(x, y)) → MARK(x)
IF_ACTIVE(true, x, y) → MARK(x)
MARK(s(x)) → MARK(x)
DIV_ACTIVE(s(x), s(y)) → IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
IF_ACTIVE(false, x, y) → MARK(y)

The TRS R consists of the following rules:

minus_active(0, y) → 0
mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
mark(s(x)) → s(mark(x))
ge_active(x, 0) → true
mark(minus(x, y)) → minus_active(x, y)
ge_active(0, s(y)) → false
mark(ge(x, y)) → ge_active(x, y)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(0, s(y)) → 0
mark(if(x, y, z)) → if_active(mark(x), y, z)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
if_active(true, x, y) → mark(x)
minus_active(x, y) → minus(x, y)
if_active(false, x, y) → mark(y)
ge_active(x, y) → ge(x, y)
if_active(x, y, z) → if(x, y, z)
div_active(x, y) → div(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule IF_ACTIVE(false, x, y) → MARK(y) we obtained the following new rules:

IF_ACTIVE(false, s(div(minus(y_3, y_4), s(y_5))), 0) → MARK(0)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Instantiation

                  ↳ QDP

                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF_ACTIVE(false, s(div(minus(y_3, y_4), s(y_5))), 0) → MARK(0)
MARK(div(x, y)) → DIV_ACTIVE(mark(x), y)
MARK(div(x, y)) → MARK(x)
MARK(s(x)) → MARK(x)
IF_ACTIVE(true, x, y) → MARK(x)
DIV_ACTIVE(s(x), s(y)) → IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)

The TRS R consists of the following rules:

minus_active(0, y) → 0
mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
mark(s(x)) → s(mark(x))
ge_active(x, 0) → true
mark(minus(x, y)) → minus_active(x, y)
ge_active(0, s(y)) → false
mark(ge(x, y)) → ge_active(x, y)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(0, s(y)) → 0
mark(if(x, y, z)) → if_active(mark(x), y, z)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
if_active(true, x, y) → mark(x)
minus_active(x, y) → minus(x, y)
if_active(false, x, y) → mark(y)
ge_active(x, y) → ge(x, y)
if_active(x, y, z) → if(x, y, z)
div_active(x, y) → div(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Instantiation

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MARK(div(x, y)) → DIV_ACTIVE(mark(x), y)
MARK(div(x, y)) → MARK(x)
MARK(s(x)) → MARK(x)
IF_ACTIVE(true, x, y) → MARK(x)
DIV_ACTIVE(s(x), s(y)) → IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)

The TRS R consists of the following rules:

minus_active(0, y) → 0
mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
mark(s(x)) → s(mark(x))
ge_active(x, 0) → true
mark(minus(x, y)) → minus_active(x, y)
ge_active(0, s(y)) → false
mark(ge(x, y)) → ge_active(x, y)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(0, s(y)) → 0
mark(if(x, y, z)) → if_active(mark(x), y, z)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
if_active(true, x, y) → mark(x)
minus_active(x, y) → minus(x, y)
if_active(false, x, y) → mark(y)
ge_active(x, y) → ge(x, y)
if_active(x, y, z) → if(x, y, z)
div_active(x, y) → div(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(div(x, y)) → MARK(x)

The remaining pairs can at least be oriented weakly.

MARK(div(x, y)) → DIV_ACTIVE(mark(x), y)
MARK(s(x)) → MARK(x)
IF_ACTIVE(true, x, y) → MARK(x)
DIV_ACTIVE(s(x), s(y)) → IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(DIV_ACTIVE(x₁, x₂)) = 1
POL(IF_ACTIVE(x₁, x₂, x₃)) = x₂
POL(MARK(x₁)) = x₁
POL(div(x₁, x₂)) = 1 + x₁
POL(div_active(x₁, x₂)) = 0
POL(false) = 0
POL(ge(x₁, x₂)) = 0
POL(ge_active(x₁, x₂)) = 0
POL(if(x₁, x₂, x₃)) = 0
POL(if_active(x₁, x₂, x₃)) = 0
POL(mark(x₁)) = 0
POL(minus(x₁, x₂)) = 0
POL(minus_active(x₁, x₂)) = 0
POL(s(x₁)) = x₁
POL(true) = 0

The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Instantiation

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ QDPOrderProof

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MARK(div(x, y)) → DIV_ACTIVE(mark(x), y)
IF_ACTIVE(true, x, y) → MARK(x)
MARK(s(x)) → MARK(x)
DIV_ACTIVE(s(x), s(y)) → IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)

The TRS R consists of the following rules:

minus_active(0, y) → 0
mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
mark(s(x)) → s(mark(x))
ge_active(x, 0) → true
mark(minus(x, y)) → minus_active(x, y)
ge_active(0, s(y)) → false
mark(ge(x, y)) → ge_active(x, y)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(0, s(y)) → 0
mark(if(x, y, z)) → if_active(mark(x), y, z)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
if_active(true, x, y) → mark(x)
minus_active(x, y) → minus(x, y)
if_active(false, x, y) → mark(y)
ge_active(x, y) → ge(x, y)
if_active(x, y, z) → if(x, y, z)
div_active(x, y) → div(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(s(x)) → MARK(x)

The remaining pairs can at least be oriented weakly.

MARK(div(x, y)) → DIV_ACTIVE(mark(x), y)
IF_ACTIVE(true, x, y) → MARK(x)
DIV_ACTIVE(s(x), s(y)) → IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(DIV_ACTIVE(x₁, x₂)) = x₁
POL(IF_ACTIVE(x₁, x₂, x₃)) = x₂
POL(MARK(x₁)) = x₁
POL(div(x₁, x₂)) = x₁
POL(div_active(x₁, x₂)) = x₁
POL(false) = 0
POL(ge(x₁, x₂)) = 0
POL(ge_active(x₁, x₂)) = 0
POL(if(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(if_active(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(mark(x₁)) = x₁
POL(minus(x₁, x₂)) = 0
POL(minus_active(x₁, x₂)) = 0
POL(s(x₁)) = 1 + x₁
POL(true) = 0

The following usable rules [17] were oriented:

mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
minus_active(0, y) → 0
ge_active(0, s(y)) → false
mark(minus(x, y)) → minus_active(x, y)
ge_active(x, 0) → true
mark(s(x)) → s(mark(x))
div_active(0, s(y)) → 0
if_active(true, x, y) → mark(x)
if_active(false, x, y) → mark(y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
mark(if(x, y, z)) → if_active(mark(x), y, z)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(ge(x, y)) → ge_active(x, y)
minus_active(x, y) → minus(x, y)
div_active(x, y) → div(x, y)
if_active(x, y, z) → if(x, y, z)
ge_active(x, y) → ge(x, y)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Instantiation

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ QDPOrderProof

                              ↳ QDP

                                ↳ Instantiation

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MARK(div(x, y)) → DIV_ACTIVE(mark(x), y)
IF_ACTIVE(true, x, y) → MARK(x)
DIV_ACTIVE(s(x), s(y)) → IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)

The TRS R consists of the following rules:

minus_active(0, y) → 0
mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
mark(s(x)) → s(mark(x))
ge_active(x, 0) → true
mark(minus(x, y)) → minus_active(x, y)
ge_active(0, s(y)) → false
mark(ge(x, y)) → ge_active(x, y)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(0, s(y)) → 0
mark(if(x, y, z)) → if_active(mark(x), y, z)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
if_active(true, x, y) → mark(x)
minus_active(x, y) → minus(x, y)
if_active(false, x, y) → mark(y)
ge_active(x, y) → ge(x, y)
if_active(x, y, z) → if(x, y, z)
div_active(x, y) → div(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule IF_ACTIVE(true, x, y) → MARK(x) we obtained the following new rules:

IF_ACTIVE(true, s(div(minus(y_3, y_4), s(y_5))), 0) → MARK(s(div(minus(y_3, y_4), s(y_5))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Instantiation

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ QDPOrderProof

                              ↳ QDP

                                ↳ Instantiation

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MARK(div(x, y)) → DIV_ACTIVE(mark(x), y)
DIV_ACTIVE(s(x), s(y)) → IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
IF_ACTIVE(true, s(div(minus(y_3, y_4), s(y_5))), 0) → MARK(s(div(minus(y_3, y_4), s(y_5))))

The TRS R consists of the following rules:

minus_active(0, y) → 0
mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
mark(s(x)) → s(mark(x))
ge_active(x, 0) → true
mark(minus(x, y)) → minus_active(x, y)
ge_active(0, s(y)) → false
mark(ge(x, y)) → ge_active(x, y)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(0, s(y)) → 0
mark(if(x, y, z)) → if_active(mark(x), y, z)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
if_active(true, x, y) → mark(x)
minus_active(x, y) → minus(x, y)
if_active(false, x, y) → mark(y)
ge_active(x, y) → ge(x, y)
if_active(x, y, z) → if(x, y, z)
div_active(x, y) → div(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 3 less nodes.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

DIV_ACTIVE(s(x), s(y)) → IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)

The remaining pairs can at least be oriented weakly.

MARK(div(x, y)) → DIV_ACTIVE(mark(x), y)
MARK(div(x, y)) → MARK(x)
MARK(s(x)) → MARK(x)
IF_ACTIVE(true, x, y) → MARK(x)

Used ordering: Matrix interpretation [3]:
Non-tuple symbols:

M( ge_active(x₁, x₂) ) =

/	0	\
\	0	/

/	1	0	\
\	1	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( minus(x₁, x₂) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( if_active(x₁, ..., x₃) ) =

/	0	\
\	0	/

/	1	0	\
\	0	0	/

x₁

/	1	0	\
\	0	1	/

x₂

/	1	0	\
\	0	1	/

x₃

M( true ) =

/	0	\
\	0	/

M( mark(x₁) ) =

/	0	\
\	0	/

/	1	0	\
\	0	1	/

x₁

M( 0 ) =

/	0	\
\	0	/

M( minus_active(x₁, x₂) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( if(x₁, ..., x₃) ) =

/	0	\
\	0	/

/	1	0	\
\	0	0	/

x₁

/	1	0	\
\	0	1	/

x₂

/	1	0	\
\	0	1	/

x₃

M( div_active(x₁, x₂) ) =

/	0	\
\	1	/

/	1	1	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( div(x₁, x₂) ) =

/	0	\
\	1	/

/	1	1	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( false ) =

/	0	\
\	0	/

M( s(x₁) ) =

/	0	\
\	1	/

/	1	0	\
\	0	0	/

x₁

M( ge(x₁, x₂) ) =

/	0	\
\	0	/

/	1	0	\
\	1	0	/

x₁

/	0	0	\
\	0	0	/

x₂

Tuple symbols:

M( MARK(x₁) ) =

[

]

x₁

M( IF_ACTIVE(x₁, ..., x₃) ) =

[

]

x₁

[

]

x₂

[

]

x₃

M( DIV_ACTIVE(x₁, x₂) ) =

[

]

x₁

[

]

x₂

Matrix type:
We used a basic matrix type which is not further parametrizeable.

As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:

mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
minus_active(0, y) → 0
ge_active(0, s(y)) → false
mark(minus(x, y)) → minus_active(x, y)
ge_active(x, 0) → true
mark(s(x)) → s(mark(x))
div_active(0, s(y)) → 0
if_active(true, x, y) → mark(x)
if_active(false, x, y) → mark(y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
mark(if(x, y, z)) → if_active(mark(x), y, z)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(ge(x, y)) → ge_active(x, y)
minus_active(x, y) → minus(x, y)
div_active(x, y) → div(x, y)
if_active(x, y, z) → if(x, y, z)
ge_active(x, y) → ge(x, y)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Instantiation

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

                        ↳ QDPOrderProof

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MARK(div(x, y)) → DIV_ACTIVE(mark(x), y)
MARK(div(x, y)) → MARK(x)
IF_ACTIVE(true, x, y) → MARK(x)
MARK(s(x)) → MARK(x)

The TRS R consists of the following rules:

minus_active(0, y) → 0
mark(0) → 0
minus_active(s(x), s(y)) → minus_active(x, y)
mark(s(x)) → s(mark(x))
ge_active(x, 0) → true
mark(minus(x, y)) → minus_active(x, y)
ge_active(0, s(y)) → false
mark(ge(x, y)) → ge_active(x, y)
ge_active(s(x), s(y)) → ge_active(x, y)
mark(div(x, y)) → div_active(mark(x), y)
div_active(0, s(y)) → 0
mark(if(x, y, z)) → if_active(mark(x), y, z)
div_active(s(x), s(y)) → if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
if_active(true, x, y) → mark(x)
minus_active(x, y) → minus(x, y)
if_active(false, x, y) → mark(y)
ge_active(x, y) → ge(x, y)
if_active(x, y, z) → if(x, y, z)
div_active(x, y) → div(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.